es:ES, i:Id, L:IdLnk List, T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e2, e1:E. loc(e1) = i  (e1 <loc e2)  ptr(("table" after e1))ptr("table" when e2)) 

latex

Definitions

t  T, P  Q, x:A. B(x), P  Q, x:AB(x), P & Q, x:AB(x), P  Q, E, A & B, loc(e), Id, s = t, Prop, (e <loc e'), b, Void, False, A, WellFnd{i}(A;x,y.R(x;y)), x,y. t(x;y), left+right, ES, Atom$n, type List, xL. P(x), e@i. P(e), A/x,y. B(x;y), 1of(t), <a,b>, vartype(i;x), , {x:A| B(x) }, (x after e), Type, {i..j}, data(T), P  Q, {T}, x. t(x), a<b, @i only events in L change   x : T, , x.A(x), let x = a in b(x), es-secret-server, IdLnk, "$x", x when e, ptr(tab), pred(e), AB, secret-table(T), f(a), Dec(P), Knd, rcv(l,tg), map(f;as), kind(e), (x  l), x:A. B(x), True, T, destination(l), source(l), first(e), s ~ t, SQType(T), @i events of kind k change x to f State(ds) (val:T), x:A. B(x), Top, EqDecider(T), IdDeq, #$n, n+m, encrypt(tab;keyv)

Lemmas

fpf-cap-single1, id-deq wf, subtype rel self, deq wf, not wf, assert wf, es-first wf, es-kind-rcv, lsrc wf, ldst wf, squash wf, true wf, es-loc-rcv, member map, decidable l member, decidable equal Kind, es-kind wf, map wf, Knd wf, rcv wf, es-after-pred, or functionality wrt iff, event system wf, IdLnk wf, es-secret-server wf, es-locl-wellfnd, le wf, all functionality wrt iff, implies functionality wrt iff, es-after wf, st-ptr wf, nat wf, es-when wf, es-vartype wf, secret-table wf, wellfounded functionality wrt iff, es-loc-pred, es-locl wf, Id wf, es-loc wf, es-E wf, es-locl-iff, es-pred wf, es-pred-locl